By securing the program it should be understood that in this disclosure, the program is written in order to guarantee operating in accordance with the specifications or the operating constraints, or that some of its (local) properties (as defined below) are proven correct. Thus, for example, in an automatic controlling equipment of a system, such as a rocket, a train, etc., it is necessary to ensure that the program executes exactly within its operating range in order to prevent jeopardy of the system or the environment thereof.
This is particularly important in complex systems because these systems, owing to their complexity, are very difficult to analyze by specialists. This difficulty may be illustrated by the accident that occurred during the first flight of the Ariane V rocket, which after expertise, turned out to be due to a thrust engine control computer. In fact, the thrust engine control computer was programmed for the previous generation rocket Ariane IV that was less powerful with less strong accelerations. The transfer of this computer onto the Ariane V rocket without taking this new parameter into consideration led the latter to receive acceleration data, which triggered an unanticipated register overflow and a motor control malfunction. Thus, it is extremely important, for critical systems, that the execution domain as well as the execution within this domain to be perfectly defined, documented and verified.
The currently used techniques are mainly based on mathematical rules based on first-order logic, or high-order logic such as Coq. The currently used techniques consist in using specific programming languages with software tools which will attempt to prove, in the mathematical sense. These software programs are called, in the literature, “provers”.
The operation of these provers fundamentally consists in transcribing the studied program into logical assertions (i.e. “proof obligations”) to be proven. Another possibility is to use the logical language itself, such as Coq, in order to describe the programs, express the properties and prove, thus avoiding the need for transformation into logical assertions.
However, it appears that the complexity, in the algorithmic sense, of the search for logic proofs increases faster than the complexity of the studied program. In the case of a computer-assisted proof, it appears that the user finds it difficult to use the intuition he has for the good operating of the program, in order to guide the prover. These techniques thus, become very difficult and high consumers of time and resources when working on critical and complicated programs, such as control programs and/or complex system where security is involved. Thus, while the need has become more important and research teams have been working on this subject for at least 30 years, these proof technologies have remained in the laboratories or are used in extremely demanding sectors regarding operational security such as aero space or rail resulting in, e.g., in this case, a software architecture which makes it difficult, if not impractible, to cut these programs into sub-assemblies that can be managed by the provers.
It would be thus advantageous to obtain a method for securing a program which would be adapted for usage on complex programs. From now on, the term “proof” (or “formal proof”) will be used as a synonym for “formal verification”, i.e., verification based on formal methods in general, and the term “logic proof” for the specific case of proof in classic logic systems (predicate logic, higher-order logic).